ds:x:Id fp Type, da:k:Knd fp Type, a:ecl(ds;da), es:ES, i:Id.
(x:Id. vartype(i;x)  ds(x)?Top)
 (e:E. loc(e) = i  valtype(e)  Valtype(da;kind(e)))
 (n:, e1, e2:{e:E| loc(e) = i }. action[[a n]][e1;e2]  ecl-es-act(es;n;a)(e1,e2)) 

latex

Definitions

t  T, x:A. B(x), P  Q, Id, Type, x. t(x), a:A fp B(a), Knd, ecl(ds;da), ES, Top, IdDeq, x.A(x), f(x)?z, vartype(i;x), x:AB(x), kind(e), Valtype(da;k), valtype(e), loc(e), s = t, E, , {x:A| B(x) }, Prop, f(a), Dec(P), decidable ecl-es-act, action[[a n]][e1;e2], x:AB(x), Atom$n, A/x,y. B(x;y), 1of(t), <a,b>, False, A, AB, , ecl-es-act(es;m;x), left+right, EqDecider(T), Unit, IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), type List, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val), AtomFree(T;x), P & Q, rec(x.A(x)), #$n, *, pred!(e;e'), SWellFounded(R(x;y)), first(e), b, loc(e), x,y. t(x;y), kind(e), , State(ds), (x  l), Void, P  Q, P  Q, P  Q, True

Lemmas

true wf, false wf, decidable ecl-es-act, l member wf, decl-state wf, bool wf, deq wf, EOrderAxioms wf, kind wf, loc wf, kindcase wf, Msg wf, unit wf, val-axiom wf, IdLnk wf, atom-free wf, assert wf, first wf, le wf, not wf, decidable wf, nat properties, nat wf, es-E wf, es-loc wf, es-valtype wf, ma-valtype wf, es-kind wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, event system wf, ecl wf, Knd wf, fpf wf, Id wf, ecl-es-act wf